es:ES, e, e':E. e loc e'   e' loc e   (e = e') 

latex

Definitions	False, P  Q, A, P  Q, P & Q, P  Q, t  T, x:A. B(x), b, e loc e' , {T}, Id, ES, (e <loc e'), E, P  Q
Lemmas	es-le wf, es-E wf, event system wf, es-axioms, or functionality wrt iff, es-le-not-locl, es-le-loc, es-loc-pred, implies functionality wrt iff, not functionality wrt iff, es-locl-iff